#include "cnf.h"
#include<string.h>
#include "sse_avx.h"
#include<stdlib.h>
#include "util.h"
#include<stdio.h>
#include"common.h"
extern variable __variables[MAX_TOT_VAR];
extern int _clause_start[MAX_TOT_VAR];
extern int _clause_varn[MAX_TOT_VAR];
clause _clause_set[MAX_CLAUSE];
variable _var_set[MAX_TOT_VAR / 10];

variable* get_var_set(cnf* cnf){
    return cnf->var_set;
}

int max_var_id = 0;
void init_ori_cnf(cnf* cnf){
    cnf->nclause = 0;
    cnf->nvar = 0;
    cnf->n_univar = 0;
    cnf->clause_set = _clause_set;
    cnf->vars = __variables;
    cnf->clause_start = _clause_start;
    cnf->clause_varn = _clause_varn;
    cnf->var_set = _var_set;
}

void add_clause(cnf*cnf, clause* cls){
    int new_cls_start;
    if (cnf->nclause > 0){
        new_cls_start = cnf->clause_start[cnf->nclause-1] 
                      + cnf->clause_varn[cnf->nclause-1];
    }else{
        new_cls_start = 0;
    }
    //printf("ckpt1 %d %d\n", new_cls_start, cls->var_num);
    clause* p = &cnf->clause_set[cnf->nclause];
    for(int i = new_cls_start; i < new_cls_start + cls->var_num; i++){
        //printf("name: %d\n", cls->vars[i-new_cls_start].name);
        copy_var(&cnf->vars[i], &cls->vars[i-new_cls_start]);
    }
    cnf->nvar += cls->var_num;
        //printf("ckpt2\n");

    p->true_val = p->true_val_available = 0;
    p->var_num = cls->var_num;
    p->vars = &cnf->vars[new_cls_start];
      //  printf("ckpt3\n");

    _bool already_contained = false;
    for(int i = 0; i < cls->var_num; i++){
        //cnf->vars[cnf->nvar++] = cls->vars[i];
        if(cls->vars[i].name > max_var_id)
            max_var_id = cls->vars[i].name;
        for(int j = 0; j < cnf->n_univar; j++){
            if (cls->vars[i].name==cnf->var_set[j].name){
                //printf("new varname: %d\n", cls->vars[i].name);
                already_contained = true; break;
            }
        }
        if (!already_contained) {
            copy_var(&cnf->var_set[cnf->n_univar], &cls->vars[i]);
            cnf->n_univar++;
        }
    }
    cnf->clause_start[cnf->nclause] = new_cls_start;
    cnf->clause_varn[cnf->nclause] = cls->var_num;
    cnf->nclause++;
} 


void init_cnf(cnf* cnf){
    
}

void print_cnf(cnf* const cnf){
    if (cnf == NULL){
        printf("print NULL \n");
        exit(0);
    }else{
        printf("cnf : %p %d\n", cnf, cnf->nclause);
    }
    if(cnf->nclause <= 0) exit(0);
    int nn = cnf->nclause > 10 ? 10 : cnf->nclause;
    for(int i = 0; i < nn; i++){
        printf("@%d ", i);
        print_clause(&cnf->clause_set[i]);
    }
    // for(int i = 0 ; i < cnf->n_univar; i++){
    //     printf("%d :ass %d, sign %d, value%d\n",
    //     cnf->var_set[i].name, cnf->var_set[i].assigned, cnf->var_set[i].sign, cnf->var_set[i].value);
    // }
    // printf("\n");
}

cnf* new_cnf_addclause(const cnf* c2, clause* cls){
    if (c2 == NULL){
        printf("c2 is NULL 1\n");
        assert(0);
    };
    cnf* c1 = NULL;
    //calculate size
    int cls_num = c2->nclause+1;
    //printf("clsnum %d cls->varnum%d\n", cls_num, cls->var_num);
    int cls_set_size, cls_start_size, cls_vn_size, cls_var_size, cls_var_set_size;
    cls_set_size = n_align(sizeof(clause) * cls_num, _ALIGN_);
    cls_start_size = n_align(sizeof(int) * cls_num, _ALIGN_);
    cls_vn_size = cls_start_size;
    cls_var_set_size = n_align(sizeof(variable) * c2->n_univar, _ALIGN_);
    cls_var_size = n_align(sizeof(variable) * (c2->nvar + cls->var_num), _ALIGN_);
    //printf("size calculated 0x%x, 0x%x, 0x%x, 0x%x, 0x%x\n", cls_set_size, cls_start_size, cls_vn_size, cls_var_size, cls_var_set_size);
    //malloc
    int totsize = sizeof(cnf) + (cls_set_size + cls_start_size + cls_vn_size + cls_var_set_size + cls_var_size);
    c1 = (cnf*)malloc(totsize);
    //printf("tot size 0x%x\n", totsize);

    //set addr
    //printf("start %p\n", (void*)c1);
    c1->clause_set = (clause*)((char*)c1 + sizeof(cnf));
    //printf("clause_set %p\n", (void*)&c1->clause_set[0]);
    c1->clause_start = (int*)((char*)&c1->clause_set[0] + cls_set_size);
    //printf("clause_start %p\n",  (void*)&c1->clause_start[0]);
    c1->clause_varn = (int*)((char*)&c1->clause_start[0] + cls_start_size);
    //printf("clause_varn %p\n",  (void*)&c1->clause_varn[0]);
    c1->vars = (variable*)((char*)&c1->clause_varn[0] + cls_vn_size);
    //printf("vars %p\n",  (void*)&c1->vars[0]);
    c1->var_set = (variable*)((char*)&c1->vars[0] + cls_var_size);
    //printf("var_set %p\n",  (void*)&c1->var_set[0]);

    //size information init
    c1->n_univar = c2->n_univar;
    c1->nclause = cls_num;//c2->nclause;
    c1->nvar = c2->nvar + cls->var_num;
    //copy
    //printf("before memcpy\n");
    // return c1;
    //printf("&c1->clause_varn[0] : %p\n", &c1->clause_varn[0]);
    for(int i = 0; i < c2->nclause; i++){
        //printf("i %d %d\n", i, c2->clause_varn[i]);
        c1->clause_varn[i] = c2->clause_varn[i];
    }
    //m_memcpy(&c1->clause_varn[0], &c2->clause_varn[0], cls_vn_size - sizeof(int) * 1);
    for(int i = 0; i < c2->nclause; i++){
        c1->clause_start[i] = c2->clause_start[i];
        assert(c1->clause_varn[i] == c2->clause_varn[i]);
    }
    //m_memcpy(&(c1->clause_start[0]), &(c2->clause_start[0]), cls_start_size - sizeof(int) * 1);
    for(int i = 0; i < c2->n_univar; i++){
        copy_var(&c1->var_set[i], &c2->var_set[i]);
    }
    for(int i = 0; i < c2->nvar; i++){
        copy_var(&c1->vars[i], &c2->vars[i]);
    }
    //m_memcpy(&c1->var_set[0], &c2->var_set[0], cls_var_set_size);
    for(int i = 0; i < c2->nclause; i++){
        int start = c1->clause_start[i];
        int num = c1->clause_varn[i];
        c1->clause_set[i].vars = &c2->vars[i];
        c1->clause_set[i].var_num = num;
        c1->clause_set[i].true_val_available = false;
    }
    //m_memcpy(&(c1->vars[0]), &(c2->vars[0]), cls_var_size - cls->var_num * sizeof(variable));
    // m_memcpy(&(c1->vars[c1->clause_start[c2->nvar - 1] + c1->clause_varn[c2->nvar - 1]]), cls->vars, sizeof(variable) * cls->var_num);
    c1->clause_varn[c2->nclause] = cls->var_num;
    c1->clause_start[c2->nclause] = c1->clause_start[c2->nvar - 1] + c1->clause_varn[c2->nvar - 1];
    for(int i = 0; i < c2->nvar; i++){
        assert(c1->vars[i].name == c2->vars[i].name);
        assert(c1->vars[i].flag == c2->vars[i].flag);
        //c1->vars[i].name = c2->vars[i].name;
        //c1->vars[i].flag = c2->vars[i].flag;
        //printf("%d, %d\n", c1->vars[i].name , c2->vars[i].name);
    }
    for(int i = 0; i < cls->var_num; i++){
        c1->vars[c2->nvar + i].name = cls->vars[i].name;
        c1->vars[c2->nvar + i].sign = cls->vars[i].sign;
        c1->vars[c2->nvar + i].assigned = cls->vars[i].assigned;
    }
    for(int i = 0; i < cls->var_num; i++){
        //printf("i:%d (%d %d)\n",i, c1->vars[c2->nvar + i].name,  cls->vars[i].name);
        assert(c1->vars[c2->nvar + i].name == cls->vars[i].name); 
    }
    for(int i = 0; i < c2->n_univar; i++){
        assert(c1->var_set[i].flag == c2->var_set[i].flag);
    }
    // for(int i = 0; i < 5; i++){
    //     printf("start %d, %d\n", c1->clause_start[i], c2->clause_start[i]);
    // }
    int index = 0;
    for(int i = 0; i < c2->nclause; i++){
        //printf("copy to c1 clause %d\n", i);
        c1->clause_set[i].true_val = c2->clause_set[i].true_val;
        c1->clause_set[i].true_val_available = c2->clause_set[i].true_val_available;
        c1->clause_set[i].vars = (variable*)&c1->vars[index];
        c1->clause_set[i].var_num = c2->clause_set[i].var_num;
        // printf("var is %d %d %d , num is %d\n", c1->vars[index].name, c1->vars[index+1].name, c1->vars[index+2].name, c1->clause_set[i].var_num);
        // printf("var is %d %d %d , num is %d\n", c2->vars[index].name, c2->vars[index+1].name, c2->vars[index+2].name, c2->clause_set[i].var_num);
        // printf("c1 ");
        // print_clause(&c1->clause_set[i]);
        // printf("c2 ");
        // print_clause(&c2->clause_set[i]);
        for(int j = 0; j < c2->clause_set[i].var_num; j++){
            //printf("%d %d %d, %d\n",i, j, c1->clause_set[i].vars[j].name, c2->clause_set[i].vars[j].name);
            assert(c1->clause_set[i].vars[j].name == c2->clause_set[i].vars[j].name);  
        }
        
        index += c1->clause_set[i].var_num;
        //printf("index %d/%d\n", index, c2->nvar);
        assert(index <= c1->nvar);
    }
    //add new one
    c1->clause_set[c2->nclause].true_val = cls->true_val;
    c1->clause_set[c2->nclause].true_val_available = false;
    c1->clause_set[c2->nclause].vars = (variable*)&c1->vars[c2->nvar];
    c1->clause_set[c2->nclause].var_num = cls->var_num;
    //print_clause(&c1->clause_set[c2->nclause]);
    assert((void*)&c1 != (void*)&c2);
    assert((void*)&c1->clause_set[0] != (void*)&c2->clause_set[0]);
    assert((void*)&c1->clause_start[0] != (void*)&c2->clause_start[0]);
    assert((void*)&c1->clause_varn[0] != (void*)&c2->clause_varn[0]);
    assert((void*)&c1->vars[0] != (void*)&c2->vars[0]);
    assert((void*)&c1->var_set[0] != (void*)&c2->var_set[0]);
    //printf("try return\n");
    return c1;//c1;
}
cnf* new_cnf_from(const cnf* c2){
    if (c2 == NULL){
        printf("c2 is NULL 2\n");
        exit(0);
    };
    //printf("copy from %p\n", (void*)c2);
    cnf* c1 = NULL;
    
    //calculate size
    //printf("%d, %d, %d \n", c2->nvar, c2->n_univar, c2->nclause);
    int cls_set_size, cls_start_size, cls_vn_size, cls_var_size, cls_var_set_size;
    cls_set_size = n_align(sizeof(clause) * c2->nclause, _ALIGN_);
    cls_start_size = n_align(sizeof(int) * c2->nclause, _ALIGN_);
    cls_vn_size = cls_start_size;
    cls_var_set_size = n_align(sizeof(variable) * c2->n_univar, _ALIGN_);
    cls_var_size = n_align(sizeof(variable) * c2->nvar, _ALIGN_);
    //printf("size calculated 0x%x, 0x%x, 0x%x, 0x%x, 0x%x\n", cls_set_size, cls_start_size, cls_vn_size, cls_var_size, cls_var_set_size);
    //malloc
    int totsize = sizeof(cnf) + (cls_set_size + cls_start_size + cls_vn_size + cls_var_set_size + cls_var_size);
    c1 = (cnf*)malloc(totsize);
    //printf("tot size 0x%x\n", totsize);

    //set addr
    //printf("start %p\n", (void*)c1);
    c1->clause_set = (clause*)((char*)c1 + sizeof(cnf));
    //printf(" %p\n", (void*)&c1->clause_set[0]);
    c1->clause_start = (int*)((char*)&c1->clause_set[0] + cls_set_size);
    //printf(" %p\n",  (void*)&c1->clause_start[0]);
    c1->clause_varn = (int*)((char*)&c1->clause_start[0] + cls_start_size);
    //printf(" %p\n",  (void*)&c1->clause_varn[0]);
    c1->vars = (variable*)((char*)&c1->clause_varn[0] + cls_vn_size);
    //printf(" %p\n",  (void*)&c1->vars[0]);
    c1->var_set = (variable*)((char*)&c1->vars[0] + cls_var_size);
    //printf(" %p\n",  (void*)&c1->var_set[0]);

    //size information init
    c1->n_univar = c2->n_univar;
    c1->nclause = c2->nclause;
    c1->nvar = c2->nvar;
    //copy
    
    // return c1;
    //m_memcpy(&c1->clause_varn[0], &c2->clause_varn[0], cls_vn_size);
    for(int i = 0; i < c2->n_univar; i++){
        copy_var(&c1->var_set[i], &c2->var_set[i]);
    }
    for(int i = 0; i < c2->nvar; i++){
        copy_var(&c1->vars[i], &c2->vars[i]);
    }
    for(int i = 0; i < c2->nclause; i++){
        //printf("i %d %d\n", i, c2->clause_varn[i]);
        c1->clause_varn[i] = c2->clause_varn[i];
    }
    //m_memcpy(&c1->clause_varn[0], &c2->clause_varn[0], cls_vn_size - sizeof(int) * 1);
    for(int i = 0; i < c2->nclause; i++){
        c1->clause_start[i] = c2->clause_start[i];
        assert(c1->clause_varn[i] == c2->clause_varn[i]);
    }
    //m_memcpy(&(c1->clause_start[0]), &(c2->clause_start[0]), cls_start_size);
    //m_memcpy(&c1->var_set[0], &c2->var_set[0], cls_var_set_size);
    //m_memcpy(&(c1->vars[0]), &(c2->vars[0]), cls_var_size);
    // printf("memcpy ok\n");
    for(int i = 0; i < c2->nvar; i++){
        assert(c1->vars[i].name == c2->vars[i].name);
        assert(c1->vars[i].flag == c2->vars[i].flag);
        //c1->vars[i].name = c2->vars[i].name;
        //c1->vars[i].flag = c2->vars[i].flag;
        //printf("%d, %d\n", c1->vars[i].name , c2->vars[i].name);
    }
    for(int i = 0; i < c2->n_univar; i++){
        assert(c1->var_set[i].flag == c2->var_set[i].flag);
    }
    // for(int i = 0; i < 5; i++){
    //     printf("start %d, %d\n", c1->clause_start[i], c2->clause_start[i]);
    // }
    int index = 0;
    for(int i = 0; i < c1->nclause; i++){
        //printf("copy to c1 clause %d\n", i);
        c1->clause_set[i].true_val = c2->clause_set[i].true_val;
        c1->clause_set[i].true_val_available = c2->clause_set[i].true_val_available;
        c1->clause_set[i].vars = (variable*)&c1->vars[index];
        c1->clause_set[i].var_num = c2->clause_set[i].var_num;
        //printf("var is %d %d %d , num is %d\n", c1->vars[index].name, c1->vars[index+1].name, c1->vars[index+2].name, c1->clause_set[i].var_num);
        //printf("var is %d %d %d , num is %d\n", c2->vars[index].name, c2->vars[index+1].name, c2->vars[index+2].name, c2->clause_set[i].var_num);
        // printf("c1 ");
        // print_clause(&c1->clause_set[i]);
        // printf("c2 ");
        // print_clause(&c2->clause_set[i]);
        for(int j = 0; j < c1->clause_set[i].var_num; j++){
            assert(c1->clause_set[i].vars[j].name == c2->clause_set[i].vars[j].name);  
        }
        
        index += c1->clause_set[i].var_num;
        //printf("index %d/%d\n", index, c2->nvar);
        assert(index <= c1->nvar);
    }
    assert((void*)&c1 != (void*)&c2);
    assert((void*)&c1->clause_set[0] != (void*)&c2->clause_set[0]);
    assert((void*)&c1->clause_start[0] != (void*)&c2->clause_start[0]);
    assert((void*)&c1->clause_varn[0] != (void*)&c2->clause_varn[0]);
    assert((void*)&c1->vars[0] != (void*)&c2->vars[0]);
    assert((void*)&c1->var_set[0] != (void*)&c2->var_set[0]);
    //printf("try return\n");
    return c1;//c1;
}

void delete_cnf(cnf* cnf){
    //printf("free delete_cnf\n");
    free(cnf);
}

unsigned count_assigned(variable* vars, int var_num){
    unsigned count = 0;
    for(int i = 0; i < var_num; i++){
        if (vars[i].assigned) count++;
    }
    return count;
}

/**
 * unset every single variable in given cnf
 */
void unset_all_vars(cnf* _cnf){
    for(int i = 0; i < _cnf->n_univar; i++){
        _cnf->var_set[i].assigned = false;
    }
    for(int i = 0; i < _cnf->nvar; i++){
        _cnf->vars[i].assigned = false;
    }
}

void _set_variable_value(cnf* cnf, int name, _bool value){
#ifdef __serial
    for(int i = 0; i < cnf->nvar; i++){
        if(name == cnf->vars[i].name){
            cnf->vars[i].assigned = true;
            cnf->vars[i].value = value;
            //printf("index %d, set flag to %d\n", i,  cnf->vars[i].flag);
        }
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if(name == cnf->var_set[i].name){
            cnf->var_set[i].assigned = true;
            cnf->var_set[i].value = value;
        }
    }
#endif 
}
